es:ES, i:Id, ds:x:Id fp Type. (x:Id. vartype(i;x) r ds(x)?Top)  (state@i r State(ds)) 

latex

Definitions	ES, t  T, Id, Type, x. t(x), x:A. B(x), a:A fp B(a), State(ds), state@i, vartype(i;x), Top, f(x)?z, IdDeq, x.A(x), x:AB(x), P  Q, P  Q, P & Q, P  Q, x initially@i , a = b, if b then t else f fi , f(a), s ~ t, False, A, s = t, , b, b, , x:A  B(x), Unit, left + right, Atom$n, let x,y = A in B(x;y), True, T
Lemmas	squash wf, true wf, subtype rel self, ifthenelse wf, es-initially wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, es-state-subtype, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-state wf, decl-state wf, fpf wf, Id wf, event system wf